/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRK30/FONT#10=ZERO30/FONT#11=BAXI30/FONT#12=MS25



␈↓ ↓H␈↓α␈↓ βFSTATING THE CORRECTNESS OF LISP PROGRAMS

␈↓ ↓H␈↓␈↓ α_In␈αprevious␈αwork␈αon␈αproving␈αthe␈αcorrectness␈αof␈αLISP␈αprograms,␈αthe␈αproperties␈αproved␈αhave
␈↓ ↓H␈↓been␈α∂chosen␈α∂somewhat␈α∂opportunistically.␈α∂ Thus␈α∂we␈α∂proved␈α∂that␈α∂␈↓↓append␈↓␈α∂is␈α∂associative␈α⊂and␈α∂that
␈↓ ↓H␈↓␈↓↓reverse[u*v] = reverse u * reverse v␈↓␈αwithout␈αclaiming␈αthat␈αthese␈αproperties␈αin␈αthemselves␈αconstitute
␈↓ ↓H␈↓the "correctness" of ␈↓↓append␈↓ or ␈↓↓reverse.␈↓

␈↓ ↓H␈↓␈↓ α_I␈α⊂don't␈α⊂believe␈α⊂there␈α⊂is␈α∂any␈α⊂general␈α⊂way␈α⊂of␈α⊂expressing␈α∂what␈α⊂is␈α⊂intuitively␈α⊂meant␈α⊂by␈α∂the
␈↓ ↓H␈↓"correctness"␈α
of␈αa␈α
computer␈α
program.␈α However,␈α
particular␈α
classes␈αof␈α
programming␈αproblems␈α
admit
␈↓ ↓H␈↓ways of formalizing correctness in logic.

␈↓ ↓H␈↓␈↓ α_Let␈αus␈α
being␈αwith␈α
sort␈αprograms,␈αbecause␈α
they␈αhave␈α
been␈αtreated␈α
extensively␈αin␈αthe␈α
program
␈↓ ↓H␈↓verification␈αliterature.␈α We␈αshall␈αbegin␈αwith␈α␈↓↓extensional␈αcorrectness␈↓,␈αi.e.␈αa␈αprogram␈αis␈αextensionally
␈↓ ↓H␈↓correct␈αif␈αit␈α
gets␈αthe␈αright␈αanswer,␈α
saying␈αnothing␈αabout␈α
how␈αmuch␈αspace␈αor␈α
time␈αit␈αuses.␈α Later␈α
we
␈↓ ↓H␈↓will␈α
discuss␈α
the␈α
method␈α∞of␈α
derived␈α
functions␈α
for␈α
getting␈α∞what␈α
we␈α
are␈α
tempted␈α
to␈α∞call␈α
␈↓↓intensional
␈↓ ↓H␈↓↓correctness␈↓␈α∪but␈α∪which␈α∪probably␈α∪more␈α∩properly␈α∪called␈α∪␈↓↓operational␈α∪correctness␈↓␈α∪or␈α∩␈↓↓computational
␈↓ ↓H␈↓↓correctness␈↓.

␈↓ ↓H␈↓␈↓ α_In␈α
LISP␈α
we␈α
shall␈α
be␈α
dealing␈αwith␈α
functions␈α
defined␈α
by␈α
conditional␈α
expression␈αrecursion,␈α
and
␈↓ ↓H␈↓the␈αcorrectness␈αis␈αa␈αrelation␈αbetween␈αthe␈αarguments␈αand␈αthe␈αvalue␈αof␈αthe␈αfunction.␈α Suppose␈α␈↓↓sort u␈↓
␈↓ ↓H␈↓is␈αa␈αsort␈αfunction.␈α
 Intuitively␈α␈↓↓sort␈↓␈αis␈αextensionally␈α
correct␈αif␈αfor␈αall␈α
lists␈α␈↓↓u␈↓␈αwhose␈αelements␈αare␈α
from
␈↓ ↓H␈↓the␈αappropriate␈αdomain,␈α␈↓↓sort u␈↓␈αis␈αdefined␈αand␈αin␈αascending␈αorder␈αand␈αhas␈αthe␈αsame␈αelements␈αas␈α␈↓↓u␈↓
␈↓ ↓H␈↓with␈αthe␈αsame␈αmultiplicities.␈α The␈αproblem␈αis␈αto␈αexpress␈αthis␈αspecification␈αformally␈αin␈αsuch␈αa␈αway
␈↓ ↓H␈↓that␈α
a␈αreader␈α
is␈αconfident␈α
that␈αthese␈α
are␈αthe␈α
correct␈αspecifications␈α
without␈αfurther␈α
proof.␈α As␈α
stated
␈↓ ↓H␈↓above,␈α
there␈α∞is␈α
always␈α∞some␈α
uncertainty␈α∞that␈α
a␈α∞formal␈α
specification␈α∞means␈α
the␈α∞same␈α
thing␈α∞as␈α
an
␈↓ ↓H␈↓informal␈αnatural␈αlanguage␈αspecification␈αjust␈αas␈αthere␈αis␈αalways␈αresidual␈αuncertainty␈αthat␈αa␈αnatural
␈↓ ↓H␈↓language specification correctly expresss what its writer "really meant".

␈↓ ↓H␈↓␈↓ α_To␈α
begin␈α
with␈α∞we␈α
want␈α
to␈α
say␈α∞that␈α
␈↓↓sort u␈↓␈α
is␈α
ordered.␈α∞ One␈α
way␈α
involves␈α
a␈α∞LISP␈α
function
␈↓ ↓H␈↓ordered that may be written

␈↓ ↓H␈↓1)␈↓ α8  ␈↓↓ordered u ← ␈↓αn␈↓↓ u ∨ ␈↓αn␈↓↓ ␈↓αd␈↓↓ u ∨ [␈↓αa␈↓↓ u ≤ ␈↓αad␈↓↓ u ∧ ordered ␈↓αd␈↓↓ u]␈↓.

␈↓ ↓H␈↓We can then prescribe

␈↓ ↓H␈↓2)␈↓ α8  ␈↓↓ordered sort u␈↓.

␈↓ ↓H␈↓If␈αthe␈αrecursive␈αdefinition␈αof␈α␈↓↓sort␈↓␈αis␈αcomplicated,␈αand␈αthe␈αuser␈αis␈αfacile␈αenough␈αwith␈αLISP␈αto␈αread
␈↓ ↓H␈↓(1)␈α
easily,␈α
a␈α
proof␈α
of␈α
(2)␈α
will␈α
substantially␈α∞increase␈α
his␈α
confidence␈α
that␈α
␈↓↓sort␈↓␈α
meets␈α
this␈α
part␈α∞of␈α
its
␈↓ ↓H␈↓specification.␈α
 In␈α
fact,␈α
he␈αmay␈α
be␈α
ready␈α
to␈α
pay␈αoff␈α
on␈α
his␈α
contract␈αfor␈α
the␈α
production␈α
of␈α
the␈αsort
␈↓ ↓H␈↓program␈αprovided␈αhe␈αis␈αequally␈αwell␈αpleased␈αwith␈αthe␈αother␈αspecifications.␈α Maybe␈αhis␈αconfidence
␈↓ ↓H␈↓can␈α∪be␈α∪increased␈α∪by␈α∪a␈α∪proof␈α∪that␈α∪␈↓↓ordered␈↓␈α∪is␈α∪total␈α∪which␈α∪can␈α∪easily␈α∪be␈α∪supplied.␈α∪ It␈α∀is␈α∪not
␈↓ ↓H␈↓immediately␈α
clear␈αwhat␈α
else␈αcould␈α
be␈α
proved␈αabout␈α
the␈αLISP␈α
predicate␈α
␈↓↓ordered␈↓␈αby␈α
itself␈αthat␈α
would
␈↓ ↓H␈↓increase␈α
his␈α
confidence,␈α
but␈α
if␈α
other␈αfunctions␈α
and␈α
predicates␈α
are␈α
available,␈α
proof␈α
of␈αsome␈α
relations
␈↓ ↓H␈↓among ␈↓↓ordered␈↓ and the others may help.

␈↓ ↓H␈↓␈↓ α_The␈αrelation␈α␈↓↓istail␈↓␈αbetween␈αtwo␈αlists␈αwill␈αprobably␈αplay␈αa␈αfundamental␈αrole␈αin␈αthe␈αtheory␈αof
␈↓ ↓H␈↓LISP␈αprograms.␈α ␈↓↓istail u v␈↓␈αis␈αtrue␈αif␈αthe␈αlist␈α␈↓↓u␈↓␈αcan␈αbe␈αobtained␈αby␈αdeleting␈αzero␈αor␈α
more␈αelements
␈↓ ↓H␈↓from the front of ␈↓↓v␈↓ and has the LISP definition
␈↓ ↓H␈↓␈↓ εH␈↓ 91


␈↓ ↓H␈↓3)␈↓ α8  ␈↓↓u istail v ← ␈↓αn␈↓↓ u ∨ u = v ∨ u istail ␈↓αd␈↓↓ v␈↓.

␈↓ ↓H␈↓␈↓ α_Its␈α∩fundamental␈α∩character␈α∩is␈α∩suggested␈α⊃by␈α∩the␈α∩fact␈α∩that␈α∩if␈α⊃␈↓↓istail␈↓␈α∩is␈α∩added␈α∩to␈α∩the␈α⊃basic
␈↓ ↓H␈↓functions␈α
of␈αLISP␈α
all␈α
other␈αLISP␈α
functions␈αcan␈α
be␈α
given␈αexplicit␈α
non-recursive␈αdefinitions.␈α
 These
␈↓ ↓H␈↓definitions␈α⊂(described␈α∂in␈α⊂McCarthy␈α∂1978)␈α⊂are␈α∂not␈α⊂computationally␈α∂useful,␈α⊂because␈α⊂they␈α∂involve
␈↓ ↓H␈↓quantifiers, but may be important in proving correctness.  Anyway we can also defined ␈↓↓ordered␈↓ by

␈↓ ↓H␈↓4)␈↓ α8  ␈↓↓ordered u ≡ ∀v1 v2.(v1 istail v2 ∧ v2 istail u ⊃ ␈↓αa␈↓↓ v1 ≤ ␈↓αa␈↓↓ v2)␈↓.

␈↓ ↓H␈↓It␈αis␈αnot␈αimmediately␈αclear␈αto␈αme␈αthat␈αthis␈αdefinition␈αof␈αordered␈αis␈αmore␈αperspicuous␈αthan␈α(1),␈αbut
␈↓ ↓H␈↓there may be some logical sense in which it is.

␈↓ ↓H␈↓␈↓ α_The␈α
second␈α∞part␈α
of␈α
the␈α∞specification␈α
of␈α∞a␈α
sort␈α
program␈α∞is␈α
more␈α
difficult.␈α∞ We␈α
need␈α∞to␈α
say
␈↓ ↓H␈↓that␈αthe␈αsorted␈αlist␈αand␈αthe␈αoriginal␈αlist␈αhave␈αthe␈αsame␈αelements␈αwith␈αthe␈αsame␈αmultiplicities.␈α One
␈↓ ↓H␈↓way␈αis␈α
to␈αsay␈αthat␈α
the␈αtwo␈αlists␈α
give␈αrise␈αto␈α
the␈αsame␈αbag␈α
or␈αmultiset.␈α An␈α
obvious␈αway␈αto␈α
represent
␈↓ ↓H␈↓the␈α
bag␈α
of␈α
a␈α
list␈α
is␈α
by␈α
sorting␈α
it,␈α
so␈α
if␈α
we␈α
have␈α
some␈α
abstract␈α
way␈α
of␈α
defining␈α
sort,␈α
then␈α∞we␈α
can
␈↓ ↓H␈↓state the correctness of ␈↓↓sort␈↓ by demanding that it be equivalent.

␈↓ ↓H␈↓␈↓ α_A more direct specification is

␈↓ ↓H␈↓␈↓ α_5)␈↓ α8  ␈↓↓∀x.(x ε u ∨ x ε sort u ⊃ multiplicity(x,u) = multiplicity(x,sort u))␈↓,

␈↓ ↓H␈↓␈↓ α_where ␈↓↓multiplicity␈↓ gets the LISP definition

␈↓ ↓H␈↓␈↓ α_6)␈↓ α8␈α∂ ␈↓↓multiplicity[x,u]␈α∂←␈α∂␈↓αif␈↓↓␈α⊂␈↓αn␈↓↓␈α∂u␈α∂␈↓αthen␈↓↓␈α∂0␈α∂␈↓αelse␈↓↓␈α⊂␈↓αif␈↓↓␈α∂x␈α∂=␈α∂␈↓αa␈↓↓␈α∂u␈α⊂␈↓αthen␈↓↓␈α∂1␈α∂+␈α∂multiplicity[x,␈↓αd␈↓↓␈α⊂u]␈α∂␈↓αelse␈↓↓
␈↓ ↓H␈↓↓multiplicity[x,␈↓αd␈↓↓ u]␈↓.

␈↓ ↓H␈↓␈↓ α_Another definition is

␈↓ ↓H␈↓␈↓ α_7)␈↓ α8  ␈↓↓multiplicity(x,u) = card {v | v istail u ∧ x = ␈↓αa␈↓↓ v}␈↓.

␈↓ ↓H␈↓␈↓ α_This␈α∩requires␈α⊃more␈α∩set␈α⊃theory␈α∩to␈α⊃manipulate␈α∩it,␈α⊃but␈α∩it␈α⊃might␈α∩be␈α⊃thought␈α∩closer␈α∩to␈α⊃the
␈↓ ↓H␈↓intuitive meaning of multiplicity.

␈↓ ↓H␈↓␈↓ α_Another␈α∪approach␈α∀is␈α∪to␈α∪axiomatize␈α∀bags␈α∪and␈α∪the␈α∀function␈α∪␈↓↓bag␈α∪u␈↓␈α∀that␈α∪gives␈α∀the␈α∪bag
␈↓ ↓H␈↓corresponding␈α⊂to␈α⊂a␈α⊂list.␈α⊂ We␈α⊂do␈α⊂not␈α⊂assume␈α⊂any␈α⊂representation␈α⊂of␈α⊂bags,␈α⊂i.e.␈α⊂our␈α⊂bag␈α⊂language
␈↓ ↓H␈↓contains␈α∃no␈α∃notation␈α∃for␈α∃arbitrary␈α∀constants.␈α∃ The␈α∃axiomatization␈α∃also␈α∃involves␈α∃a␈α∀function
␈↓ ↓H␈↓␈↓↓mult(x,z)␈↓␈α∞giving␈α∂the␈α∞multiplicity␈α∞of␈α∂the␈α∞element␈α∞␈↓↓x␈↓␈α∂in␈α∞the␈α∞bag␈α∂␈↓↓z.␈↓␈α∞ Here␈α∞are␈α∂some␈α∞axioms␈α∂and␈α∞a
␈↓ ↓H␈↓schema:

␈↓ ↓H␈↓␈↓ α_␈↓↓∀z1 z2.(∀x.(mult(x,z1) = mult(x,z2)) ⊃ z1 = z2)␈↓

␈↓ ↓H␈↓␈↓ α_␈↓↓∀z x.(mult(x,adjoin(x,z)) = 1 + mult(x,z))␈↓

␈↓ ↓H␈↓␈↓ α_␈↓↓∀x.(mult(x,Zerobag) = 0)␈↓

␈↓ ↓H␈↓␈↓ α_␈↓↓qF(Zerobag) ∧ ∀x z.(qF(z) ⊃ qF(adjoin(x,z))) ⊃ ∀z.qF(z)␈↓

␈↓ ↓H␈↓␈↓ α_␈↓↓∀u.(bag u = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ zerobag ␈↓αelse␈↓↓ adjoin(␈↓αa␈↓↓ u, bag ␈↓αd␈↓↓ u))␈↓
␈↓ ↓H␈↓␈↓ εH␈↓ 92


␈↓ ↓H␈↓␈↓ α_At␈α∩some␈α⊃point␈α∩we␈α⊃are␈α∩dependent␈α⊃on␈α∩a␈α⊃theorem␈α∩or␈α⊃metatheorem␈α∩to␈α⊃the␈α∩effect␈α∩that␈α⊃the
␈↓ ↓H␈↓axiomatized␈αfunctions␈αexist.␈α This␈αcan␈αbe␈αdemonstrated␈αby␈αrepresenting␈αthem␈αas␈αlists␈αand␈αproving
␈↓ ↓H␈↓that some sort function satisfies the axioms for ␈↓↓bag u␈↓.

␈↓ ↓H␈↓␈↓ α_If␈αI␈αunderstand␈αit␈αcorrectly,␈αthe␈αStanford␈αVerification␈αGroup's␈αtreatment␈αof␈αsorting␈αinvolves
␈↓ ↓H␈↓axiomatizing␈α
the␈α
predicate␈α␈↓↓permutes(u,v)␈↓␈α
which␈α
asserts␈α
that␈αthe␈α
array␈α
␈↓↓A␈↓␈αis␈α
a␈α
permutation␈α
of␈αthe
␈↓ ↓H␈↓array ␈↓↓B.␈↓  This seems to me to be more peculiar to sorting than the approaches suggested here.

␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Artificial Intelligence Laboratory
␈↓ ↓H␈↓Computer Science Department
␈↓ ↓H␈↓Stanford University
␈↓ ↓H␈↓Stanford, California 94305

␈↓ ↓H␈↓ARPANET: MCCARTHY@SU-AI

␈↓ ↓H␈↓␈↓ α_␈↓εThis draft of CORREC[S78,JMC] PUBbed at 18:31 on May 16, 1978.␈↓